COM: well_fnd_summary

COM: well_fnd_intro

ABS: WellFnd{i}(A;x,y.R(x;y))

STM: wellfounded wf

COM: INV_IMAGE_com

STM: inv image ind a

STM: inv image ind tp

STM: inv image ind

COM: WFND_FUNCTIONALITY_tcom

STM: comb for wellfounded wf

STM: wellfounded functionality wrt implies

STM: wellfounded functionality wrt iff

COM: well_fnd_end

Up	Standard, Standard